|
| 1: |
|
sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) |
→ sortSu(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t))))) |
| 2: |
|
sortSu(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) |
→ sortSu(cons(te(a),sortSu(circ(sortSu(s),sortSu(t))))) |
| 3: |
|
sortSu(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(sop(lift),sortSu(t))))) |
→ sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))) |
| 4: |
|
sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) |
→ sortSu(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) |
| 5: |
|
sortSu(circ(sortSu(s),sortSu(id))) |
→ sortSu(s) |
| 6: |
|
sortSu(circ(sortSu(id),sortSu(s))) |
→ sortSu(s) |
| 7: |
|
sortSu(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) |
→ sortSu(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u))) |
| 8: |
|
te(subst(te(a),sortSu(id))) |
→ te(a) |
| 9: |
|
te(msubst(te(a),sortSu(id))) |
→ te(a) |
| 10: |
|
te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) |
→ te(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) |
|
There are 14 dependency pairs:
|
| 11: |
|
SORTSU(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) |
→ SORTSU(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t))))) |
| 12: |
|
SORTSU(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) |
→ TE(msubst(te(a),sortSu(t))) |
| 13: |
|
SORTSU(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) |
→ SORTSU(circ(sortSu(s),sortSu(t))) |
| 14: |
|
SORTSU(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) |
→ SORTSU(cons(te(a),sortSu(circ(sortSu(s),sortSu(t))))) |
| 15: |
|
SORTSU(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) |
→ SORTSU(circ(sortSu(s),sortSu(t))) |
| 16: |
|
SORTSU(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(sop(lift),sortSu(t))))) |
→ SORTSU(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))) |
| 17: |
|
SORTSU(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(sop(lift),sortSu(t))))) |
→ SORTSU(circ(sortSu(s),sortSu(t))) |
| 18: |
|
SORTSU(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) |
→ SORTSU(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) |
| 19: |
|
SORTSU(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) |
→ SORTSU(circ(sortSu(t),sortSu(u))) |
| 20: |
|
SORTSU(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) |
→ SORTSU(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u))) |
| 21: |
|
SORTSU(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) |
→ SORTSU(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))) |
| 22: |
|
SORTSU(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) |
→ SORTSU(circ(sortSu(s),sortSu(t))) |
| 23: |
|
TE(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) |
→ TE(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) |
| 24: |
|
TE(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) |
→ SORTSU(circ(sortSu(s),sortSu(t))) |
|
The approximated dependency graph contains one SCC:
{12,13,15,17-20,22-24}.